e<e'.P(e) == e:es-E(es). es-locl(es; e; e')  P(e) 

latex

---

clarification:

alle-lt(es;e';e.P(e)) == e:es-E(es). es-locl(es; e; e')  P(e) 

latex

Definitions	x:A. B(x), es-E(es), P  Q, es-locl(es; e; e')
FDL editor aliases	alle-lt